(declare-fun h () a)
(declare-fun i () a)
(declare-fun j () a)
(declare-fun k () b)
(declare-fun l () b)
(declare-fun m () b)
(declare-fun n () c)
(declare-fun o () c)
(declare-fun p () c)
(assert (or (distinct (ite ((_ is cons) (cons (ite ((_ is cons) (ite ((_ is cons) l) l e)) (car (ite ((_ is cons) l) l e)) (g q)) (ite ((_ is f) p) (children p) e))) (cdr (cons (ite ((_ is cons) (ite ((_ is cons) l) l e)) (car (ite ((_ is cons) l) l e)) (g q)) (ite ((_ is f) p) (children p) e))) e) (cons (f (ite ((_ is f) (g (ite ((_ is d) j) j q))) (children (g (ite ((_ is d) j) j q))) e)) e)) (= i h) (distinct o (f (cons n (cons (g i) m)))) (distinct k (ite ((_ is cons) l) l e)) (= h j)))
(assert (= o (f l)))
(check-sat)
